d-comp(D;v;sched;dec)(t,f)
== let s = i.if t=0 x.M(i).init(x)?v(i,x) else 1of(f(t-1,i)) fi in 
== i.let si = s(i) in 
== i.let w = d-partial-world(D;f;t;s) in 
== i.let a = Case sched(i) of
== i.let a = inl(f)  Case f(t) of
== i.let a = inl(f)  inl(l)  if destination(l) = i  0<||queue(l;t)||
== i.let a = inl(f)  inl(l)  if doact(rcv(l,mtag(hd(queue(l;t))));mval(hd(queue(l;t))))
== i.let a = inl(f)  inl(l)  else null fi
== i.let a = inl(f)  inr(a)  if isl(dec(i,a,si)) doact(inr(a);outl(dec(i,a,si))) else null fi
== i.let a = inr(x)  null in 
== i.let m = if isl(a) nil
== i.let m = else filter(m.source(mlnk(m)) = i;M(i).sends(1of(outr(a)),si,2of(outr(a)))) fi in 
== i.let s' = if isl(a) si else x.M(i).ef(1of(outr(a)),x,si,2of(outr(a)))?si(x) fi in 
== i.<s',a,m> 

latex

---

clarification:

d-comp(D;v;sched;dec)(t,f)
== let s = i.if t=0 x.d-m(D; i).init(x)?v(i,x) else 1of(f(t-1,i)) fi in 
== i.let si = s(i) in 
== i.let w = d-partial-world(D;f;t;s) in 
== i.let a = Case sched(i) of
== i.let a = inl(f)  Case f(t) of
== i.let a = inl(f)  inl(l)  if destination(l) = i  0<||w-queue(w; l; t)||
== i.let a = inl(f)  inl(l)  if doact(rcv(l,mtag(hd(w-queue(w; l; t))))
== i.let a = inl(f)  inl(l)  if doact;mval(hd(w-queue(w; l; t))))
== i.let a = inl(f)  inl(l)  else null fi
== i.let a = inl(f)  inr(a)  if isl(dec(i,a,si)) doact(inr(a);outl(dec(i,a,si))) else null fi
== i.let a = inr(x)  null in 
== i.let m = if isl(a) nil
== i.let m = else filter(m.source(mlnk(m)) = i
== i.let m = else filter;d-m(D; i).sends(1of(outr(a)),si,2of(outr(a)))) fi in 
== i.let s' = if isl(a) si else x.d-m(D; i).ef(1of(outr(a)),x,si,2of(outr(a)))?si(x) fi in 
== i.<s',a,m> 

latex

Definitions	i=j, M.init(x)?v, n-m, d-partial-world(D;f;t';s), Case b of inl(x)  s(x) ; inr(y)  t(y), p  q, i = j, destination(l), i<j, #$n, ||as||, rcv(l,tg), mtag(m), mval(m), hd(l), queue(l;t), doact(k;v), inr(x), outl(x), null, nil, filter(P;l), a = b, source(l), mlnk(m), M.sends(k,s,v), let x = a in b(x), if b t else f fi, isl(x), x.A(x), M.ef(k,x,s,v)?w, M(i), 1of(t), 2of(t), outr(x), f(a), <a,b>
FDL editor aliases	d-comp